let f (x : int) = 
  predicate p = (x = x) in
    assert p in
    x
